(DEFUN HELLO ()
  (PRINT 'HELLO))
